We study the automatic synthesis of fair non-repudiation protocols, a classof fair exchange protocols, used for digital contract signing. First, we showhow to specify the objectives of the participating agents and the trusted thirdparty (TTP) as path formulas in LTL and prove that the satisfaction of theseobjectives imply fairness; a property required of fair exchange protocols. Wethen show that weak (co-operative) co-synthesis and classical (strictlycompetitive) co-synthesis fail, whereas assume-guarantee synthesis (AGS)succeeds. We demonstrate the success of assume-guarantee synthesis as follows:(a) any solution of assume-guarantee synthesis is attack-free; no subset ofparticipants can violate the objectives of the other participants; (b) theAsokan-Shoup-Waidner (ASW) certified mail protocol that has knownvulnerabilities is not a solution of AGS; (c) the Kremer-Markowitch (KM)non-repudiation protocol is a solution of AGS; and (d) AGS presents a new andsymmetric fair non-repudiation protocol that is attack-free. To our knowledgethis is the first application of synthesis to fair non-repudiation protocols,and our results show how synthesis can both automatically discovervulnerabilities in protocols and generate correct protocols. The solution toassume-guarantee synthesis can be computed efficiently as the secureequilibrium solution of three-player graph games.
展开▼
